Skip to content

normal_prob cont./reproductive property#1955

Open
affeldt-aist wants to merge 3 commits into
math-comp:masterfrom
affeldt-aist:normal_20260426
Open

normal_prob cont./reproductive property#1955
affeldt-aist wants to merge 3 commits into
math-comp:masterfrom
affeldt-aist:normal_20260426

Conversation

@affeldt-aist
Copy link
Copy Markdown
Member

@affeldt-aist affeldt-aist commented Apr 27, 2026

Motivation for this change

This PR provides a proof of the continuity of normal_prob and of the reproductive
property of normal distribution:
Screenshot 2026-04-27 at 11 00 37

This is taken from the PR #1712
and it relies on the field tactic (fyi: @proux01 )

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

@affeldt-aist affeldt-aist added this to the 1.17.0 milestone Apr 27, 2026
@affeldt-aist affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Apr 27, 2026
Copy link
Copy Markdown
Collaborator

@IshiguroYoshihiro IshiguroYoshihiro left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks good for me.
I think there is some room for generalization on auxiliary lemmas, but I don't think it need to block this PR.

Comment thread theories/probability_theory/normal_distribution.v Outdated
Comment thread theories/probability_theory/normal_distribution.v Outdated
Comment thread theories/probability_theory/normal_distribution.v Outdated
Comment thread theories/probability_theory/normal_distribution.v Outdated
Comment thread theories/probability_theory/normal_distribution.v Outdated
Comment thread theories/probability_theory/normal_distribution.v
affeldt-aist and others added 3 commits June 5, 2026 16:39
Co-authored-by: IshiguroYoshihiro <jb.15r.1213@s.thers.ac.jp>
@affeldt-aist
Copy link
Copy Markdown
Member Author

@IshiguroYoshihiro Thank you very much for the comments!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement ✨ This issue/PR is about adding new features enhancing the library

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants